While I understand (and agree with) the idea of this change, it'll break third-party code if it depends on this interface structure. Therefore I would be very careful with it and only introduce it on a major version change.

Has AbelianGroup actually be implemented anywhere outside of this repo? My guess is that it has not, although I would be interested to see any examples in the wild.

I certainly implemented it once or twice. Probably still have the code somewhere on my disk. ;) But I understand your point. It's probably right.

These kinds of rearrangements are painful. There's this discrepancy between how we intuitively think about addition (actually about all operations that are simultaneously commutative and associative) as a list of terms, where exact sequencing does not matter. On the other hand in the AST it's represented as a tree, rather than a list, which makes moving terms around much more, well not exactly difficult, but troublesome I'd say. I've been dreaming for some time now of a view (i.e. specific type) allowing to express such lengthy sums (or products, or whatever) as a list of terms. I tried to do it myself once, but I got stuck on the way of proving properties of such views. Maybe you'd like to try doing it? Having such a type, we could even devise some syntax sugar to make such rearrangements even more intuitive…

It would be nice to have something like that, but I don't know how. I've just been grinding through on a case-by-case basis.

I imagine it would be a type containing a List (or Vect) of terms, with a proof that folding it is the same as a regular use of the function you fold with. It should only require associativity I guess? Then you can implement transformations on the List, proving they still don't change the result (this is where commutativity will be required. I have tried something like this:

data Sum : Type -> Type where
    MkSum : Monoid a => List a -> Sum a

eval : Sum a -> a
terms : Sum a -> List a

evalEquvalentToFold : Monoid s => (s : Sum a) -> eval s = fold (<+>) Algebra.neutral  (terms s)

Unfortunately proving anything about fold is difficult due to the way it's implemented. Probably a slightly different approach would be required, but I think this is the right direction.

Unfortunately I don't know the answer to your question.

However, I'm definitely against committing commented-out code to the master. If it does not work, for whatever reason, it shouldn't be committed. Perhaps you could propose it as a separate PR after this one is done, so that every one can pull the branch in question and investigate more easily?

I cut the code, but left the implementation line commented out as a clue for the future.

This property is called distributivity. Maybe mtimesDistributesOverGroupOp?

I suppose that is technically true, but the spirit of the operation is that it's exponentiation when the group op is interpreted as multiplication, or multiplication when it's interpreted as addition.

I can't see, how does it matter. Exponentiation does indeed distribute over multiplication. But mtimesDistributesOverGroupOp mentions neither addition nor multiplication explicitly, so it should be ok.

Isn't this just a special case of commutativity of ZZ addition? I mean plusCommutativeZ (gtimes n x) (gtimes m x) has exactly this type, doesn't it?

No, gtimes n x produces an instance of the group type, not a ZZ.